l1, l2:IdLnk, dt:tg:Id fp Type, tg:Id, T:Type.
lnk-decl(l1;dt)(rcv(l2,tg))?T ~ if l1 = l2 then dt(tg)?T else T fi  

latex

Definitions	t  T, IdLnk, s = t, , x:A. B(x), b, Type, A, b, , a = b, x:AB(x), P  Q, x:A  B(x), P & Q, P  Q, Unit, left + right, Id, x. t(x), a:A fp B(a), {T}, SQType(T), s ~ t, lnk-decl(l;dt), Knd, x.A(x), Top, rcv(l,tg), KindDeq, x  dom(f), f(x)?z, False, f(x)
Lemmas	lnk-decl-dom2, fpf-dom wf, Kind-deq wf, rcv wf, fpf-trivial-subtype-top, Knd wf, lnk-decl wf, IdLnk sq, lnk-decl-cap, fpf wf, Id wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-lnk, eq lnk wf, bool wf, bnot wf, not wf, assert wf, IdLnk wf